es:ES, R:{R:EE| e, e':E. R(e,e')  (e' < e)} , d:(e, e':E. Dec(R(e,e'))).
causal-predecessor(es;es-r-pred{i:l}(es;d;R))
& (e:E.
& (((can-apply(es-r-pred{i:l}(es;d;R);e))  (e':E. R(e,e')))
& (& ((can-apply(es-r-pred{i:l}(es;d;R);e))  R(e,do-apply(es-r-pred{i:l}(es;d;R);e)))) 

latex

Definitions

ES, es-r-pred{i:l}(es;d;R), causal-pred-from-relation, Dec(P), {x:A| B(x)} , (e < e'), Type, x(s1,s2), P & Q, P  Q, f(a), causal-predecessor(es;p), left + right, Top, E, , s = t, x:A. B(x), P  Q, x:AB(x), t  T, x:A. B(x), x:A  B(x), b